/* 
 * Copyright 2014 Josef Hertl.
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *      http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */
package caetus.modelChecking.role;

import caetus.modelChecking.goal.ModelGoalMap;
import caetus.modelChecking.transition.TransitionAction;
import caetus.modelChecking.transition.TransitionActionEnum;
import caetus.modelChecking.transition.TransitionMaker;
import caetus.modelChecking.variable.ModelBaseVariable;
import caetus.modelChecking.variable.ModelConstants;
import caetus.modelChecking.variable.ModelEncryptedVariable;
import caetus.modelChecking.variable.ModelVariable;
import caetus.modelChecking.variable.ModelVariableType;
import caetus.pkcs11.tokenCapabilities.TokenCapabilities;
import caetus.pkcs11.tokenCapabilities.TokenCapability;
import caetus.pkcs11.tokenCapabilities.TokenCapabilityGroup;
import java.util.LinkedList;
import java.util.List;

/**
 * Represents a token - never an intruder.
 *
 * @author Josef Hertl
 */
public class ModelToken extends ModelActor {

    public ModelToken(ModelVariable playedByAgent, String name, TokenCapabilities capabilities) {
        super(playedByAgent, name, capabilities);
    }

    @Override
    protected String makeTransitions() {
        String result = "\ntransition\n\n";
        int ordinal = 1;

        //Preparation of start actions - effectively replaces initialization
        List<TransitionAction> startActionList = new LinkedList<TransitionAction>();
        startActionList.add(new TransitionAction(1));//the transition to state 1
        if (capabilities.capabilityGroupWorking(TokenCapabilityGroup.SYMMETRIC_CRYPTOGRAPHY)) {
            startActionList.add(new TransitionAction(TransitionActionEnum.GENERATE, findVariable("LSK")));
            startActionList.add(new TransitionAction(TransitionActionEnum.SECRET, findVariable("LSK"), true));
        }
        if (capabilities.capabilityGroupWorking(TokenCapabilityGroup.ASYMMETRIC_CRYPTOGRAPHY)) {
            startActionList.add(new TransitionAction(TransitionActionEnum.GENERATE, findVariable("LPuK")));
            startActionList.add(new TransitionAction(TransitionActionEnum.GENERATE_PRIVATE_KEY, findVariable("LPrK")));
            startActionList.add(new TransitionAction(TransitionActionEnum.SEND_PLAIN, findVariable("LPuK"), true));
            startActionList.add(new TransitionAction(TransitionActionEnum.SECRET, findVariable("LPrK"), true));
        }
        TransitionAction[] startActions = new TransitionAction[startActionList.size()];
        for (int i = 0; i < startActions.length; i++) {
            startActions[i] = startActionList.get(i);
        }
        result += TransitionMaker.makeTransition(ordinal, 0, new TransitionAction("start"), startActions);
        ordinal++;

        //symmetric cryptography section
        if (capabilities.capabilityGroupWorking(TokenCapabilityGroup.SYMMETRIC_CRYPTOGRAPHY)) {
            //Symmetric decryption
            if (capabilities.capabilityWorking(TokenCapability.SYMMETRIC_ENCRYPTION_DECRYPTION)) {
                //decryption by SK - the decryption does not take an input command, it simply decrypts the input data if it is encrypted by a given key
                if (capabilities.capabilityWorking(TokenCapability.SYMMETRIC_WRAPPING_KEY_CAN_DECRYPT)) {
                    result += TransitionMaker.makeStateOneTransition(ordinal, new TransitionAction(TransitionActionEnum.RECEIVE_VARIABLE, new ModelEncryptedVariable(findVariable("M"), true, findVariable("SK"))), new TransitionAction[]{new TransitionAction(TransitionActionEnum.SEND_PLAIN, findVariable("M"), true)});
                    ordinal++;
                }
                //decryption by LSK - should be always possible, as long as decryption works
                result += TransitionMaker.makeStateOneTransition(ordinal, new TransitionAction(TransitionActionEnum.RECEIVE_VARIABLE, new ModelEncryptedVariable(findVariable("M"), true, findVariable("LSK"))), new TransitionAction[]{new TransitionAction(TransitionActionEnum.SEND_PLAIN, findVariable("M"), true)});
                ordinal++;
                if (capabilities.capabilityWorking(TokenCapability.SYMMETRIC_CREATED_KEY_CAN_DECRYPT)) {
                    //decryption by ISK
                    result += TransitionMaker.makeStateOneTransition(ordinal, new TransitionAction(TransitionActionEnum.RECEIVE_VARIABLE, new ModelEncryptedVariable(findVariable("M"), true, findVariable("ISK"))), new TransitionAction[]{new TransitionAction(TransitionActionEnum.SEND_PLAIN, findVariable("M"), true)});
                    ordinal++;
                }
            }
            //Symmetric encryption
            if (capabilities.capabilityWorking(TokenCapability.SYMMETRIC_ENCRYPTION_DECRYPTION)) {
                //encryption by SK - no input command
                result += TransitionMaker.makeStateOneTransition(ordinal, new TransitionAction(TransitionActionEnum.RECEIVE_VARIABLE, findVariable("M")), new TransitionAction[]{new TransitionAction(TransitionActionEnum.SEND_ENCRYPTED, findVariable("M"), findVariable("SK"))});
                ordinal++;
                //encryption by LSK
                result += TransitionMaker.makeStateOneTransition(ordinal, new TransitionAction(TransitionActionEnum.RECEIVE_VARIABLE, findVariable("M")), new TransitionAction[]{new TransitionAction(TransitionActionEnum.SEND_ENCRYPTED, findVariable("M"), findVariable("LSK"))});
                ordinal++;
                if (findVariable("ISK") != null) {
                    //decryption by ISK
                    result += TransitionMaker.makeStateOneTransition(ordinal, new TransitionAction(TransitionActionEnum.RECEIVE_VARIABLE, findVariable("M")), new TransitionAction[]{new TransitionAction(TransitionActionEnum.SEND_ENCRYPTED, findVariable("M"), findVariable("ISK"))});
                    ordinal++;
                }
            }
            //Symmetric key wrap
            if (capabilities.capabilityWorking(TokenCapability.WRAPPING_SYMMETRIC_BY_SYMMETRIC)) {
                //wrap by SK
                if (capabilities.capabilityWorking(TokenCapability.SYMMETRIC_WRAPPING_KEY_CAN_WRAP)) {
                    result += TransitionMaker.makeStateOneTransition(ordinal, new TransitionAction("wrap_secret_by_secret_sk"), new TransitionAction[]{new TransitionAction(TransitionActionEnum.SEND_ENCRYPTED, findVariable("LSK"), findVariable("SK"))});
                    ordinal++;
                }
                //unwrap by SK
                if (capabilities.capabilityWorking(TokenCapability.SYMMETRIC_WRAPPING_KEY_CAN_UNWRAP)) {
                    result += TransitionMaker.makeStateOneTransition(ordinal, new TransitionAction(TransitionActionEnum.RECEIVE_VARIABLE, new ModelEncryptedVariable(findVariable("LSK"), true, findVariable("SK"))), new TransitionAction[]{new TransitionAction(TransitionActionEnum.SEND_PLAIN, ModelConstants.getConstant("unwrap_success"), false)});
                    ordinal++;
                }
                //unwrap by ISK, automatically presumes the unwrapped key is LSK
                if (capabilities.capabilityWorking(TokenCapability.CREATE_SYMMETRIC) && capabilities.capabilityWorking(TokenCapability.SYMMETRIC_CREATED_KEY_CAN_UNWRAP)) {
                    result += TransitionMaker.makeStateOneTransition(ordinal, new TransitionAction(TransitionActionEnum.RECEIVE_VARIABLE, new ModelEncryptedVariable(findVariable("LSK"), true, findVariable("ISK"))), new TransitionAction[]{new TransitionAction(TransitionActionEnum.SEND_PLAIN, ModelConstants.getConstant("unwrap_success"), false)});
                    ordinal++;
                }
            }
        }

        //Asymmetric section
        if (capabilities.capabilityGroupWorking(TokenCapabilityGroup.ASYMMETRIC_CRYPTOGRAPHY)) {
            //asymmetric encryption
            //encryption by PuK - no input command
            result += TransitionMaker.makeStateOneTransition(ordinal, new TransitionAction(TransitionActionEnum.RECEIVE_VARIABLE, findVariable("M")), new TransitionAction[]{new TransitionAction(TransitionActionEnum.SEND_ENCRYPTED, findVariable("M"), findVariable("PuK"))});
            ordinal++;
            //encryption by LPuK
            result += TransitionMaker.makeStateOneTransition(ordinal, new TransitionAction(TransitionActionEnum.RECEIVE_VARIABLE, findVariable("M")), new TransitionAction[]{new TransitionAction(TransitionActionEnum.SEND_ENCRYPTED, findVariable("M"), findVariable("LPuK"))});
            ordinal++;
            if (findVariable("IPuK") != null) {
                //decryption by IPuK
                result += TransitionMaker.makeStateOneTransition(ordinal, new TransitionAction(TransitionActionEnum.RECEIVE_VARIABLE, findVariable("M")), new TransitionAction[]{new TransitionAction(TransitionActionEnum.SEND_ENCRYPTED, findVariable("M"), findVariable("IPuK"))});
                ordinal++;
            }

            //Asymmetric decryption
            if (capabilities.capabilityWorking(TokenCapability.ASYMMETRIC_ENCRYPTION_DECRYPTION)) {
                if (capabilities.capabilityWorking(TokenCapability.ASYMMETRIC_WRAPPING_KEY_CAN_DECRYPT)) {
                    //decryption by PrK
                    result += TransitionMaker.makeStateOneTransition(ordinal, new TransitionAction(TransitionActionEnum.RECEIVE_VARIABLE, new ModelEncryptedVariable(findVariable("M"), true, findVariable("PuK"))), new TransitionAction[]{new TransitionAction(TransitionActionEnum.SEND_PLAIN, findVariable("M"), true)});
                    ordinal++;
                }
                //decryption by LPrK - always should be possible
                result += TransitionMaker.makeStateOneTransition(ordinal, new TransitionAction(TransitionActionEnum.RECEIVE_VARIABLE, new ModelEncryptedVariable(findVariable("M"), true, findVariable("LPuK"))), new TransitionAction[]{new TransitionAction(TransitionActionEnum.SEND_PLAIN, findVariable("M"), true)});
                ordinal++;
            }
        }

        //combination of symmetric and asymmetric
        if (capabilities.capabilityGroupWorking(TokenCapabilityGroup.SYMMETRIC_CRYPTOGRAPHY) && capabilities.capabilityGroupWorking(TokenCapabilityGroup.ASYMMETRIC_CRYPTOGRAPHY)) {
            //symmetric by asymmetric wrapping
            if (capabilities.capabilityWorking(TokenCapability.WRAPPING_SYMMETRIC_BY_ASYMMETRIC)) {
                if (capabilities.capabilityWorking(TokenCapability.ASYMMETRIC_WRAPPING_KEY_CAN_WRAP)) {
                    //wrap LSK by PuK
                    result += TransitionMaker.makeStateOneTransition(ordinal, new TransitionAction("wrap_secret_by_public"), new TransitionAction[]{new TransitionAction(TransitionActionEnum.SEND_ENCRYPTED, findVariable("LSK"), findVariable("PuK")), new TransitionAction(TransitionActionEnum.SECRET, findVariable("LSK"))});
                    ordinal++;
                }
                if (capabilities.capabilityWorking(TokenCapability.ASYMMETRIC_WRAPPING_KEY_CAN_UNWRAP)) {
                    //unwrap LSK by PrK
                    result += TransitionMaker.makeStateOneTransition(ordinal, new TransitionAction(TransitionActionEnum.RECEIVE_VARIABLE, new ModelEncryptedVariable(findVariable("LSK"), true, findVariable("PuK"))), new TransitionAction[]{new TransitionAction(TransitionActionEnum.SEND_PLAIN, ModelConstants.getConstant("unwrap_success"), false)});
                    ordinal++;
                }
            }
            //asymmetric by symmetric wrapping
            if (capabilities.capabilityWorking(TokenCapability.WRAPPING_ASYMMETRIC_BY_SYMMETRIC)) {
                //wrap LPrK by SK
                if (capabilities.capabilityWorking(TokenCapability.SYMMETRIC_WRAPPING_KEY_CAN_WRAP)) {
                    result += TransitionMaker.makeStateOneTransition(ordinal, new TransitionAction("wrap_private_by_secret_sk"), new TransitionAction[]{new TransitionAction(TransitionActionEnum.SEND_ENCRYPTED, findVariable("LPrK"), findVariable("SK"))});
                    ordinal++;
                }
                //unwrap LPrK by SK
                if (capabilities.capabilityWorking(TokenCapability.SYMMETRIC_WRAPPING_KEY_CAN_UNWRAP)) {
                    result += TransitionMaker.makeStateOneTransition(ordinal, new TransitionAction(TransitionActionEnum.RECEIVE_VARIABLE, new ModelEncryptedVariable(findVariable("LPrK"), true, findVariable("SK"))), new TransitionAction[]{new TransitionAction(TransitionActionEnum.SEND_PLAIN, ModelConstants.getConstant("unwrap_success"), false)});
                    ordinal++;
                }
                //unwrap LPrK by ISK, automatically presumes the unwrapped key is LPK
                if (capabilities.capabilityWorking(TokenCapability.CREATE_SYMMETRIC) && capabilities.capabilityWorking(TokenCapability.SYMMETRIC_CREATED_KEY_CAN_UNWRAP)) {
                    result += TransitionMaker.makeStateOneTransition(ordinal, new TransitionAction(TransitionActionEnum.RECEIVE_VARIABLE, new ModelEncryptedVariable(findVariable("LPrK"), true, findVariable("ISK"))), new TransitionAction[]{new TransitionAction(TransitionActionEnum.SEND_PLAIN, ModelConstants.getConstant("unwrap_success"), false)});
                    ordinal++;
                }
            }
        }

        //obvious weakness - makes sure the model checker actually find the attack
        if (capabilities.capabilityWorking(TokenCapability.OBVIOUS_WEAKNESS)) {
            result += TransitionMaker.makeStateOneTransition(ordinal, new TransitionAction("show_weakness"), new TransitionAction[]{new TransitionAction(TransitionActionEnum.SEND_PLAIN, findVariable("LSK"))});
            ordinal++;
        }
        return result;
    }

    @Override
    public void generateLocalVariables() {
        ModelBaseVariable M = new ModelBaseVariable("M", ModelVariableType.MESSAGE);
        addLocalVariable(M);
        if (capabilities.capabilityGroupWorking(TokenCapabilityGroup.SYMMETRIC_CRYPTOGRAPHY)) {
            ModelBaseVariable LSK = new ModelBaseVariable("LSK", ModelVariableType.SYMMETRIC_KEY); //the secret key that may be exchanged. It is automatically considered sensitive.
            addLocalVariable(LSK);
            ModelGoalMap.addVariableToSecretGoals(LSK);
        }
        if (capabilities.capabilityGroupWorking(TokenCapabilityGroup.ASYMMETRIC_CRYPTOGRAPHY)) {
            ModelVariable LPuK = new ModelBaseVariable("LPuK", ModelVariableType.PUBLIC_KEY); //the public key that will be generated
            addLocalVariable(LPuK);
            ModelBaseVariable LPrK = new ModelBaseVariable("LPrK", ModelVariableType.PRIVATE_KEY); //the secret key that may be exchanged. It is automatically considered sensitive.
            addLocalVariable(LPrK);
            ModelGoalMap.addVariableToSecretGoals(LPrK);
        }
        addLocalVariable(new ModelBaseVariable("State", ModelVariableType.NAT));
    }

    @Override
    protected String prepareInit() {
        String result = "\ninit ";
        result += findVariable("State") + " := 0";
        result += "\n\n";
        return result;
    }
}
